﻿// The MIT License (MIT)
//
// Copyright (c) 2019 Henk-Jan Lebbink
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:

// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.

// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.

namespace AsmSim
{
    using System.Diagnostics.Contracts;
    using Microsoft.Z3;

    public class BranchInfo
    {
        public readonly BoolExpr BranchCondition;
        public readonly string Key;
        public readonly bool BranchTaken;

        public BranchInfo(BoolExpr condition, bool taken)
        {
            Contract.Requires(condition != null);

            this.BranchCondition = condition;
            this.Key = condition.ToString();
            this.BranchTaken = taken;
        }

        public BranchInfo Translate(Context ctx)
        {
            return new BranchInfo(this.BranchCondition.Translate(ctx) as BoolExpr, this.BranchTaken);
        }

        public BoolExpr GetData(Context ctx)
        {
            Contract.Requires(ctx != null);
            if (false)
            {
                BoolExpr bc = this.BranchCondition.Translate(ctx) as BoolExpr;
                return this.BranchTaken ? bc : ctx.MkNot(bc);
            }
            else
            {
                return this.BranchTaken ? this.BranchCondition : ctx.MkNot(this.BranchCondition);
            }
        }

        public override string ToString()
        {
            return "BranchInfo: " + this.BranchCondition + "\n(branch taken " + this.BranchTaken + ")";
        }
    }
}
